Refactors the `structure` command to support recursive structures. These are disabled for now, pending additional elaborator support in leanprover#5822. This refactor is also a step toward `structure` appearing in `mutual` blocks.

Error reporting is now more precise, and this fixes an issue where general errors could appear on the last field.

Closes leanprover#2512

Refactors the `structure` command to support recursive structures. These
are disabled for now, pending additional elaborator support in #5822.
This refactor is also a step toward `structure` appearing in `mutual`
blocks.

Error reporting is now more precise, and this fixes an issue where
general errors could appear on the last field. Adds "don't know how to
synthesize placeholder" errors for default values.

Closes #2512

Refactors the `structure` command to support recursive structures. These
are disabled for now, pending additional elaborator support in leanprover#5822.
This refactor is also a step toward `structure` appearing in `mutual`
blocks.

Error reporting is now more precise, and this fixes an issue where
general errors could appear on the last field. Adds "don't know how to
synthesize placeholder" errors for default values.

Closes leanprover#2512

Now that the elaborator supports primitive projections for recursive
inductive types (#5822), enable defining recursive inductive types with
the `structure` command, which was set up in #5842.

Example:
```lean
structure Tree where
  n : Nat
  children : Fin n → Tree

def Tree.size : Tree → Nat
  | {n, children} => Id.run do
    let mut s := 0
    for h : i in [0 : n] do
      s := s + (children ⟨i, h.2⟩).size
    pure s
```

Note for kernel re-implementors: recursive structures are exercising the
kernel feature where primitive projections are valid for one-constructor
inductive types in general, so long as the structure isn't a `Prop` and
doesn't have any non-`Prop` fields, not just ones that are non-indexed
and non-recursive.

Closes #2512